\section{Completeness}

\subsection{The Logic $\mathbf{M}_\mathrm{tc0}$}

\frame
{
  \hframetitle{The Logic $\mathbf{M}_\mathrm{tc0}$}
\vfill
In the subsequent discussion, ``tc'' stands for \alert{test conditional}.
\vfill
  $\mathbf{M}_\mathrm{tc0}$ is the logic built up from:
\vfill
  \begin{itemize}
  \item The $\vdash_\mathrm{tc0}$ syntactic entailment relation defined by the
        $\mathit{M}_\mathrm{tc0}$ sequent system
  \item The $\vDash_{tc0}$ semantic entailment relation
  \end{itemize}
\vfill
}


\frame
{
  \frametitle{The $\mathit{M}_\mathrm{tc0}$ Sequent System}

  This system has the following \alert{logical rules}...
  \[
    \frac{\Gamma, \varphi_i \Rightarrow \chi}
         {\Gamma, \varphi_1 \land \varphi_2 \Rightarrow \chi}
         ~\mathrm{L}^i_\land \quad
    \frac{\Gamma \Rightarrow \varphi_1 \quad \Gamma \Rightarrow \varphi_2}
         {\Gamma \Rightarrow \varphi_1 \land \varphi_2}
         ~\mathrm{R}_\land \quad
    \frac{\Gamma \Rightarrow \varphi}
         {\Gamma, \neg \varphi \Rightarrow \bot}
         ~\mathrm{L}_\neg
  \] \[
    \frac{\Gamma, \varphi \Rightarrow \bot}
         {\Gamma \Rightarrow \neg \varphi}
         ~\mathrm{R}_\neg \qquad
    \frac{\Gamma, \varphi \Rightarrow \chi}
         {\Gamma, \neg \neg \varphi \Rightarrow \chi}
         ~\mathrm{L}_{\neg\neg}
  \]

  ...and the following \alert{structural rules}:
  \[
    \frac{\Gamma \Rightarrow \bot}
         {\Gamma \Rightarrow \varphi}
         ~R_\mathrm{mon} \quad
    \frac{\Gamma, \varphi, \varphi, \Delta \Rightarrow \chi}
         {\Gamma, \varphi, \Delta \Rightarrow \chi}
         ~\mathit{Contr} \quad
    \frac{\Gamma, \Delta \Rightarrow \chi}
         {\Gamma, \varphi, \Delta \Rightarrow \chi}
         ~\mathit{Mon}
  \] \[
    \frac{\Gamma, \varphi, \psi, \Delta \Rightarrow \chi}
         {\Gamma, \psi, \varphi, \Delta \Rightarrow \chi}
         ~\mathit{Perm}
  \]
}

\frame
{
  \frametitle{The $\vDash_\mathrm{tc0}$ Relation}

  Let $\mathbf{I}$ be a class of models, $\mathcal{I} \in \mathbf{I}$, and
  let $\Pi \Rightarrow \psi$ be an argument such that $\varphi \in \Pi, \psi$
  are $\mathcal{L}_0$ terms.

  \vfill
  $\mathcal{I} \vDash_\mathrm{tc0} \Pi \Rightarrow \psi$ iff for all
  $\alpha \in \mathcal{I}$: if $\alpha [\varphi] = \alpha$ for each $\varphi \in \Pi$ then
  $\alpha [\psi] = \alpha$
}

\frame
{
  \frametitle{Soundness and Completeness}

  The soundness and completeness of $M_{tc0}$ follow Proposition 4.4 and
  Proposition 4.5 in \citep{van_der_does_updatemight_1997}, respectively.
}

\subsection{The Logic $\mathbf{M}_\mathrm{tc\Box}$}

\frame
{
  \hframetitle{The Logic $\mathbf{M}_\mathrm{tc\Box}$}

  $\mathbf{M}_\mathrm{tc\Box}$ is the logic built up from:
  \begin{itemize}
      \item The $\vdash_\mathrm{tc\Box}$ syntactic entailment relation defined
        by the $\mathit{M}_\mathrm{tc\Box}$ sequent system
      \item The $\vDash_{tc\Box}$ semantic entailment relation
        
  \end{itemize}
}


\frame
{
  \frametitle{The $\mathit{M}_\mathrm{tc\Box}$ Sequent System}

  Along with the logical rules of $\mathit{M}_\mathrm{tc0}$, the
  system $\mathit{M}_\mathrm{tc\Box}$
  has the following \alert{additional} rules:
  \[
    \frac{\Gamma, \varphi \Rightarrow \chi}
         {\Gamma, \Box \varphi \Rightarrow \chi}
         ~\mathrm{L}_\Box \qquad
    \frac{\Gamma \Rightarrow \varphi}
         {\Gamma \Rightarrow \Box \varphi}
         ~\mathrm{R}_\Box
  \]

  ...and the following \alert{structural rules}:
  \[
    \frac{\Gamma \Rightarrow \bot}
         {\Gamma \Rightarrow \varphi}
         ~R_\mathrm{mon} \quad
    \frac{\Gamma, \Delta \Rightarrow \chi}
         {\Gamma, \varphi, \Delta \Rightarrow \chi}
         ~\mathit{Mon} \quad
    \frac{\Gamma, \varphi, \psi, \Delta \Rightarrow \chi}
         {\Gamma, \psi, \varphi, \Delta \Rightarrow \chi}
         ~\mathit{Perm}
  \]
}

\frame
{
  \frametitle{The $\vDash_\mathrm{tc\Box}$ Relation}

  Let $\mathbf{I}$ be a class of models, $\mathcal{I} \in \mathbf{I}$, and
  let $\Pi \Rightarrow \psi$ be an argument such that $\varphi \in \Pi, \psi$
  are $\mathcal{L}_\Box$ terms.

  \vfill
  $\mathcal{I} \vDash_\mathrm{tc0} \Pi \Rightarrow \psi$ iff for all
  $\alpha \in \mathcal{I}$: if $\alpha [\varphi] = \alpha$ for each $\varphi \in \Pi$ then
  $\alpha [\psi] = \alpha$
}

\begin{frame}
  \frametitle{Soundness}

  \begin{theorem}[Soundness]
    The system $\mathit{M}_\mathrm{tc\Box}$ is sound with respect to the
    class of all models: if $\Pi \vdash_\mathrm{tc\Box} \tau$ then $\Pi
    \vDash_\mathrm{tc\Box} \tau$.
  \end{theorem}
\end{frame}

\begin{frame}[allowframebreaks]
  \proofframetitle{Soundness (Proof)}
  \begin{proof}
    By Proposition 4.4 of \citep{van_der_does_updatemight_1997}
    all the rules of $\mathit{M}_\mathrm{tc0}$ are sound. So we only need to
    consider the new rules $L_{\Box}$ and $R_{\Box}$:

  \begin{itemize}
    \item $L_{\Box}$. Assume that $\mathcal{I} \vDash_\mathrm{tc\Box} \Delta,
      \varphi \Rightarrow \psi$, which means that for every $\alpha \in
      \mathcal{I}$, if $\alpha [\Delta, \varphi] = \alpha$ then $\alpha [\psi] = \alpha$. Derive a
      contradiction by assuming that there is some $\beta \in \mathcal{I}$ such that
      (i) $\beta [\Delta] = \beta$, (ii) $\beta [\Box \varphi] = \beta$ and (iii) $\beta [\psi]
      \neq \beta$. But (ii) implies that $\beta [\varphi] = \beta$ by the $\Box$-reduction
      lemma. This combined with (i) gives us that $\beta [\Delta, \varphi] = \beta
      [\Delta] [\varphi] = \beta [\varphi] = \beta$. So $\beta [\psi] = \beta$ by assumption.
      $\blitz$ with (iii)! So $\mathcal{I} \vDash_\mathrm{tc\Box} \Delta,
      \Box \varphi \Rightarrow \psi$.
  
  \framebreak

    \item $R_{\Box}$. Assume that $\mathcal{I} \vDash_\mathrm{tc\Box} \Pi
      \Rightarrow \varphi$, which means that for every $\alpha \in \mathcal{I}$, if
      $\alpha [\Pi] = \alpha$ then $\alpha [\varphi] = \alpha$. Derive a contradiction by assuming
      that there is some $\beta \in \mathcal{I}$ such that (i) $\beta [\Pi] = \beta$ and
      (ii) $\beta [\Box \varphi] \neq \beta$. Then the $\Box$-reduction lemma gives us
      that (ii) implies $\beta [\varphi] \neq \beta$. $\blitz$ so $\mathcal{I}
      \vDash_\mathrm{tc\Box} \Pi \Rightarrow \Box \varphi$. 
  \end{itemize}
  \end{proof}
\end{frame}

\begin{frame}
  \frametitle{Completeness Lemma}

  \begin{definition}
  We define $\Pi^\bullet$ to be $\Pi$ with all $\Box$ operators erased. For
  example $(\varphi, \Box \psi)^\bullet = (\varphi, \psi)$.
  \end{definition}

  \begin{lemma}
    If $\Pi \nvdash_{\mathrm{tc\Box}} \tau$ then $\Pi^\bullet
    \nvdash_{\mathrm{tc\Box}} \tau^\bullet$.
\end{lemma}
\end{frame}    
\begin{frame}
  \proofframetitle{Completeness Lemma (Proof)}
    \begin{proof}
      By contradiction. Assume $\Pi \nvdash_{\mathrm{tc\Box}} \tau$ and suppose
      that $\Pi^\bullet \vdash_{\mathrm{tc\Box}} \tau^\bullet$. By using
      Perm and $L_{\Box}$ we can add our $\Box$-operator to all the elements of
      $\Pi^\bullet$ that had a $\Box$ in front of them in $\Pi$. So now we
      have $\Pi \vdash_{\mathrm{tc\Box}} \tau^\bullet$. Then by $R_{\Box}$ we
      can add our $\Box$-operator to $\tau^\bullet$ if there was a $\Box$ in
      $\tau$. But then $\Pi \vdash_{\mathrm{tc\Box}} \tau$. $\blitz$ therefore $\Pi^\bullet \nvdash_{\mathrm{tc\Box}} \tau^\bullet$.
    \end{proof}
\end{frame}

\begin{frame}
\frametitle{Completeness}

  We will need some propositions from \citep{van_der_does_updatemight_1997}:
  \begin{itemize}
    \item Proposition 3.6 (iii): $\alpha [\Gamma] = \alpha$ iff for all $m \in \alpha$: $m(
      \Gamma) = 1$.
    \item Proposition 3.5 (iv): $\mathbf{1}[\Gamma] = \mathbf{0}$ iff $\Gamma
      \vdash_\mathrm{cpl} \bot$.
  \end{itemize}

  \begin{theorem}[Completeness]
    If $\Pi \vDash_{\mathrm{tc\Box}} \tau$ then $\Pi \vdash_{\mathrm{tc\Box}}
    \tau$.
  \end{theorem}
\end{frame}

\begin{frame}[allowframebreaks]
  \proofframetitle{Completeness (Proof)}
  \begin{proof}
    We prove the contrapositive, so assume $\Pi \nvdash_{\mathrm{tc\Box}} \tau$.
    Then by the lemma $\Pi^\bullet \nvdash_{\mathrm{tc\Box}} \tau^\bullet$.
    Let $\mathcal{P} \supseteq \mathrm{PROP} (\Pi, \tau)$ be a set of proposition
    letters, containing those occurring in $\Pi$ and $\tau$. Then by classical
    completeness we have $\Pi^\bullet \nvDash_{\mathrm{tc\Box}} \tau^\bullet$.
    Let $m \subseteq \mathcal{P}$, a set of true proposition letters, be a
    model such that $m (\Pi^\bullet) = 1$ and $m (\tau^\bullet) = 0$. If
    we can extend this model such that $m (\Pi) = 1$ and $m (\tau) = 0$ we are
    done. So we must find a world $\alpha \subseteq \wp ( \mathcal{P})$ with $\alpha
    [\Pi] = \alpha$ and $\alpha [\tau] \neq \alpha$, which will be our model. We make a case
    distinction on the presence of $\Box$-operators in $\tau$.
  \framebreak
  \begin{itemize}
    \item $\tau \in \mathcal{L}_0$. Then $\tau$ does not contain a
      $\Box$-operator, $\tau = \tau^\bullet$. Consider $\alpha = \mathbf{1}
      [\Pi^\bullet]$. Then $m \in \alpha$, but $m \not\in \alpha [\tau]$. Then by
      Proposition 3.6 (iii) because $m \in \alpha$ 
      and $m (\tau) \neq 1$ we have $\alpha [\tau] \neq \alpha$. We still need to have
      $\alpha [\sigma] = \alpha$ for all $\sigma$ in $\Pi$. If $\sigma$ does not have a
      $\Box$-operator, then this follows from Proposition 3.6 (iii) because $\alpha
      \subseteq \mathbf{1} [\Pi^\bullet] \subseteq \mathbf{1} [\sigma]$. If it does then
      let $\Pi \equiv \Pi', \Box \varphi, \Pi''$ (so $\sigma =\Box \varphi$).
      But then because $\varphi$ is in $\Pi^\bullet$ we have $\alpha [\varphi] =
      \alpha$ and by $\Box$-reduction $\alpha [\Box \varphi] = \alpha$.

  \framebreak
  
    \item $\tau \not\in \mathcal{L}_0$. Then $\tau$ contains a $\Box$-operator,
      $\tau \neq \tau^\bullet$. Consider $\alpha = \mathbf{1} [\neg \tau^\bullet,
      \Pi^\bullet]$. By proposition 3.6 (iv) we have $\alpha [\tau^\bullet] =
      \mathbf{0}$, because $\neg \tau^\bullet, \Pi^\bullet, \tau^\bullet
      \vdash_\mathrm{cpl} \bot$. So $\alpha [\tau] = \mathbf{0}$, by definition of $\Box$.
      Furthermore $\alpha [\tau] \neq \alpha$, because $m (\tau^\bullet) = 0
      \Leftrightarrow m (\neg \tau^\bullet) = 1$ and $m (\Pi^\bullet) = 1$ so
      $m (\neg \tau^\bullet \wedge \Pi^\bullet) = 1$ and therefore $m \in \alpha$.
      We still need to have $\alpha [\sigma] = \alpha$ for all $\sigma$ in $\Pi$.
      As before there is no issue if $\sigma$ is in $\Pi^\bullet$. So suppose
      $\Pi \equiv \Pi', \Box \varphi, \Pi''$. Then because $\varphi$ is in
      $\Pi^\bullet$ we have $\alpha [\varphi] = \alpha$ and by $\Box$-reduction
      $\alpha [\Box \varphi] = \alpha$. 
  \end{itemize}
  \end{proof}
\end{frame}

\begin{frame}
  \frametitle{Important Observation}

  Because of the \alert{$\gillies$-reduction lemma} we already have a logic for
  $\gillies$. However, the operator does not occur in the grammar as such.
  So we introduce a new logic in which it does.
\end{frame}

\subsection{The Logic $\mathbf{M}_\mathrm{tc\gillies}$}

\frame
{
  \hframetitle{The Logic $\mathbf{M}_\mathrm{tc\gillies}$}

  Like $\mathbf{M}_\mathrm{tc\Box}$, the logic  $\mathbf{M}_\mathrm{tc\gillies}$ is built up from:
  
  \begin{itemize}
  \item The $\vdash_\mathrm{tc\gillies}$ syntactic entailment relation defined
        by the $\mathit{M}_\mathrm{tc\gillies}$ sequent system
  \item The $\vDash_{tc\gillies}$ semantic entailment relation
  \end{itemize}

The $\vDash_\mathrm{tc\gillies}$ relation is defined just as before with
$\vDash_\mathrm{tc\Box}$.  The only novelty we really introduce is a
modification of the sequence calculus we previously introduced.
}

\frame
{
  \frametitle{The $\mathit{M}_\mathrm{tc\gillies}$ Sequent System}
The system $\mathit{M}_\mathrm{tc\gillies}$ has all of the rules of
$\mathit{M}_\mathrm{tc0}$ along with the following:
  \[
    \frac{\Gamma, \varphi \to \psi \Rightarrow \chi}
         {\Gamma, \varphi \gillies \psi \Rightarrow \chi}
         ~\mathrm{L}_\gillies \qquad
    \frac{\Gamma \Rightarrow \varphi \to \psi}
         {\Gamma \Rightarrow \varphi \gillies \psi}
         ~\mathrm{R}_\gillies
  \]

  And it has the same structural rules as $\mathit{M}_\mathrm{tc\Box}$.
}

\begin{frame}
\frametitle{Soundness \& Completeness}

  \begin{theorem}[Soundness]
    The system $\mathit{M}_\mathrm{tc\gillies}$ is sound with respect to the
    class of all models: if $\Pi \vdash_\mathrm{tc\gillies} \tau$ then $\Pi
    \vDash_\mathrm{tc\gillies} \tau$.
  \end{theorem}

  \begin{theorem}[Completeness]
    If $\Pi \vDash_{\mathrm{tc\gillies}} \tau$ then $\Pi
    \vdash_{\mathrm{tc\gillies}} \tau$.
  \end{theorem}
\end{frame}

\begin{frame}
  \proofframetitle{Soundness \& Completeness (Proof)}
\begin{proof}
The proofs proceed exactly as the proofs for the same results for
$\mathbf{M}_\mathrm{tc\Box}$ were formulated, the only difference is
that rather than employing the $\Box$-reduction lemma, the
$\gillies$-reduction lemma is employed instead.
\end{proof}
\end{frame}

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "beamer"
%%% End: 
